COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% These axioms reify goals and actions.  They enable us to prove
C00011 ENDMK
C⊗;
% These axioms reify goals and actions.  They enable us to prove
% should(I,prog(walk(car),drive(airport)),S0)

% Warning: These axioms haven't been checked to see that misguided subsitutions
% (e.g. using a situation as a person) can't give strange results.
% The axioms can be complicated by adding premisses to ensure that
% situations are never substituted for variables standing for persons,
% but the sort mechanism (which will be explained later) does it better.

declare INDVAR x y z s p a1 a2 g a;

declare INDCONST I, S0, desk, home,car,airport,county;

declare PREDCONST att 2, walkable 1, drivable 1;

declare PREDCONST holds 2, wants 3, should 3;

declare OPCONST at 2, result 3, prog 2, walk 1, drive 1;

axiom walkable:	walkable(home);;

axiom drivable:	drivable(county);;

axiom at:
	holds(at(I,desk),S0)
	att(desk,home)
	holds(at(car,home),S0)
	att(home,county)
	att(airport,county)
;;

axiom ats:	∀x y.(att(x,y) ⊃ ∀s.holds(at(x,y),s));;

axiom attrans:
	∀x y z s.(holds(at(x,y),s) ∧ holds(at(y,z),s) ⊃ holds(at(x,z),s))
	∀x y z.(att(x,y) ∧ att(y,z) ⊃ att(x,z))
;;

axiom notI:	¬(I=desk) ∧ ¬(I=car) ∧ ¬(I=home) ∧ ¬(I=airport);;

axiom walk:
	∀x y z p s.((walkable(x) ∧ (att(y,x)∨holds(at(y,x),s)) ∧ (att(z,x)
				∨ holds(at(z,x),s))
			 ∧ holds(at(p,y),s))
		⊃ (holds(at(p,z),result(p,walk(z),s))
		   ∧ ∀x y.(¬(x = I) 
		⊃ (holds(at(x,y),result(p,walk(z),s)) ≡ holds(at(x,y),s)))))
;;

axiom drive:
	∀x y z p s.((drivable(x) ∧ att(y,x) 
				∧ att(z,x) ∧ holds(at(car,y),s) 
					∧ holds(at(p,car),s))
		⊃ (holds(at(car,z),result(p,drive(z),s))
		∧ ∀x y.(¬(x = car ∨ holds(at(x,car),s)) ∨ y=car
			 ⊃ (holds(at(x,y),result(p,drive(z),s)) 
					≡ holds(at(x,y),s)))))
;;

axiom prog:
	∀a1 a2 p s.(result(p,prog(a1,a2),s) = result(p,a2,result(p,a1,s)))
;;

axiom should:
	∀p g a s.(wants(p,g,s) ∧ holds(g,result(p,a,s)) ⊃ should(p,a,s))
;;

axiom want:
	wants(I,at(I,airport),S0)
;;


Here are the actual commands that generated the proof.

fetch airpo6.ax;
∀e walk home desk car I S0;
∀e drive county home airport I result(I,walk(car),S0);
∀e attrans1 I car airport result(I,drive(airport),result(I,walk(car),S0));
tauteq 1:#2#2 walkable at1 at2 at3 1;
∀e ↑ car home;
tauteq 2:#2#2 walkable drivable at1 at2 at3 at4 at5 notI 1:5;
∀e ↑ I car;
tauteq holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0)))
1:7 notI walkable drivable at1 at2 at3 at4 at5;
∀e prog walk(car) drive(airport) I S0;
substr 9 in 8;
∀e should I at(I,airport) prog(walk(car),drive(airport)) S0;
taut 11:#2 10 11 want;


Here is the proof as printed by FOL.

*****∀E walk home,desk,car,I,S0;

1 (walkable(home)∧((att(desk,home)∨holds(at(desk,home),S0))∧((att(car,home)∨holds(at(car,home),S0))∧holds(at(I,d%
esk),S0))))⊃(holds(at(I,car),result(I,walk(car),S0))∧∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(a%
t(x,y),S0))))  

*****∀E drive county,home,airport,I,result(I,walk(car),S0);

2 (drivable(county)∧(att(home,county)∧(att(airport,county)∧(holds(at(car,home),result(I,walk(car),S0))∧holds(at(%
I,car),result(I,walk(car),S0))))))⊃(holds(at(car,airport),result(I,drive(airport),result(I,walk(car),S0)))∧∀x y.%
((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport),result(I,walk(c%
ar),S0)))≡holds(at(x,y),result(I,walk(car),S0)))))  

*****∀E attrans1 I,car,airport,result(I,drive(airport),result(I,walk(car),S0));

3 (holds(at(I,car),result(I,drive(airport),result(I,walk(car),S0)))∧holds(at(car,airport),result(I,drive(airport%
),result(I,walk(car),S0))))⊃holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0)))  

*****TAUTEQ ∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(at(x,y),S0))) walkable,at1,at2,at3,1;

4 ∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(at(x,y),S0)))  

*****∀E ↑ car,home;

5 ¬(car=I)⊃(holds(at(car,home),result(I,walk(car),S0))≡holds(at(car,home),S0))  

*****TAUTEQ ∀x y.((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport%
),result(I,walk(car),S0)))≡holds(at(x,y),result(I,walk(car),S0)))) walkable,drivable,at1,at2,at3,at4,at5,notI,1:%
5;

6 ∀x y.((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport),result(I%
,walk(car),S0)))≡holds(at(x,y),result(I,walk(car),S0))))  

*****∀E ↑ I,car;

7 (¬(I=car∨holds(at(I,car),result(I,walk(car),S0)))∨car=car)⊃(holds(at(I,car),result(I,drive(airport),result(I,w%
alk(car),S0)))≡holds(at(I,car),result(I,walk(car),S0)))  

*****TAUTEQ holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0))) notI,walkable,drivable,at1,at2,%
at3,at4,at5,1:7;

8 holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0)))  

*****∀E prog walk(car),drive(airport),I,S0;

9 result(I,prog(walk(car),drive(airport)),S0)=result(I,drive(airport),result(I,walk(car),S0))  

*****SUBSTR ↑ IN ↑↑;

10 holds(at(I,airport),result(I,prog(walk(car),drive(airport)),S0))  

*****∀E should I,at(I,airport),prog(walk(car),drive(airport)),S0;

11 (wants(I,at(I,airport),S0)∧holds(at(I,airport),result(I,prog(walk(car),drive(airport)),S0)))⊃should(I,prog(wa%
lk(car),drive(airport)),S0)  

*****TAUT should(I,prog(walk(car),drive(airport)),S0) want,10:11;

12 should(I,prog(walk(car),drive(airport)),S0)